We looked at Calculi and for all the Calculi we'll see that you kind of take the propositional

Calculus as a backbone and then you have to do something about the quantifiers.

And almost always that means you have to do arbitrary substitutions for the universal

variables and witness substitutions for the existentials.

So you have to typically have, for every quantifier you have to have one rule.

And this is just the natural data, oops, what's that?

No, I don't want any dictionaries.

We looked at examples, we looked at sequence, we looked at equality and we looked at a big

proof.

Well, big for this course.

Big proofs nowadays are things which are too big for two slides, they're too big for a

thousand slides, they're in the giga to terabyte range and take up to say 20 person years to

develop.

Those are big proofs.

And then there are still very big proofs.

I think the biggest so far is they've proven a conjecture which had, what was it, I think

it was 50 terabytes in size which is about 50 terabyte steps.

You don't want to read them.

This one you can still read and see, yes, that's a proof.

For everything else you just basically, for the big proofs you need machines to check

this.

And that's the important thing about proofs.

If you have full information, you have full justifications, you can actually go and check

the rules.

You can say whether say a rule like that is at work.

And you can build very simple programs that can do the checking for you.

That gives you a big deal of safety.

And that is really what is being done in safety critical things like program verification

or something like this.

Where you want to verify that there are no bugs in your program or that your program

has certain properties.

It may delete your hard disk but it's never going to insult your mother.

Those are things you can prove.

If there is a proof like that, you can have your own little program that actually checks

whether the proof applies to that program.

Those are the things that in many industrial strength applications are now being used.

And you need a logic that's at least as strong as first order logic to do this.

Because almost all programming languages can compute with numbers.

So you need something at least first order strong.

Whereas hardware verification you can do with propositional logic.

You can translate a chip into a huge propositional logic formula.

And then say something about it, typically.

Except of course if you have memory then you probably want to have something stronger as

well.

And there are special logics for that.